Left Termination of the query pattern
times(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

(0) Obligation:

Clauses:

times(X, Y, Z) :- mult(X, Y, 0, Z).
mult(0, Y, 0, 0).
mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z).
mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z).

Query: times(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="K: times(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: times(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: mult(T7, T8, 0, T10)\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 1 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2 | mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: mult(T7, T8, 0, T10), SCOPE: 2, CLAUSE: 3\n\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="I: mult(T28, T29, T29, T31)\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 1 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 1\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2 | mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 2\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: mult(T28, T29, T29, T31), SCOPE: 3, CLAUSE: 3\n\nT28 is ground\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="A: mult(T51, 0, 0, T54)\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 1 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 1\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2 | mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 2\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: mult(T51, 0, 0, T54), SCOPE: 4, CLAUSE: 3\n\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: mult(T63, 0, 0, T65)\n\nT63 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: mult(T75, s(T77), T77, T79)\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 1 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 1\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2 | mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 2\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: mult(T75, s(T77), T77, T79), SCOPE: 5, CLAUSE: 3\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="B: mult(T99, s(0), s(0), T102)\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 1 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 2 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 2 | mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: mult(T99, s(0), s(0), T102), SCOPE: 6, CLAUSE: 3\n\nT99 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: mult(T108, s(0), 0, T110)\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 1 | mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 2 | mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 3\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 1\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 2 | mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 3\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 2\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: mult(T108, s(0), 0, T110), SCOPE: 7, CLAUSE: 3\n\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: mult(T119, s(0), s(0), T121)\n\nT119 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: mult(T131, s(s(T133)), T133, T135)\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 1 | mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 2 | mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 1\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 2 | mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 2\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: mult(T131, s(s(T133)), T133, T135), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="C: mult(T155, s(s(0)), s(s(0)), T158)\n\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 1 | mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 2 | mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 3\n\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 2 | mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 3\n\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: mult(T155, s(s(0)), s(s(0)), T158), SCOPE: 9, CLAUSE: 3\n\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: mult(T164, s(s(0)), s(0), T166)\n\nT164 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 1 | mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 2 | mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 3\n\nT164 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 2 | mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 3\n\nT164 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: mult(T164, s(s(0)), s(0), T166), SCOPE: 10, CLAUSE: 3\n\nT164 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: mult(T172, s(s(0)), 0, T174)\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 1 | mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 2 | mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 3\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 1\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 2 | mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 3\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 2\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: mult(T172, s(s(0)), 0, T174), SCOPE: 11, CLAUSE: 3\n\nT172 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: mult(T183, s(s(0)), s(s(0)), T185)\n\nT183 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: mult(T195, s(s(s(T197))), T197, T199)\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 1 | mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 2 | mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 3\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 1\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 2 | mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 3\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 2\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: mult(T195, s(s(s(T197))), T197, T199), SCOPE: 12, CLAUSE: 3\n\nT195 is ground\nT197 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="D: mult(T219, s(s(s(0))), s(s(s(0))), T222)\n\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 1 | mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 2 | mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 3\n\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 2 | mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 3\n\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: mult(T219, s(s(s(0))), s(s(s(0))), T222), SCOPE: 13, CLAUSE: 3\n\nT219 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: mult(T228, s(s(s(0))), s(s(0)), T230)\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 1 | mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 2 | mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 3\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 2 | mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 3\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: mult(T228, s(s(s(0))), s(s(0)), T230), SCOPE: 14, CLAUSE: 3\n\nT228 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: mult(T236, s(s(s(0))), s(0), T238)\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 1 | mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 2 | mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 3\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 2 | mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 3\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: mult(T236, s(s(s(0))), s(0), T238), SCOPE: 15, CLAUSE: 3\n\nT236 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: mult(T244, s(s(s(0))), 0, T246)\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 1 | mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 2 | mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 3\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 1\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 2 | mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 3\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 2\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: mult(T244, s(s(s(0))), 0, T246), SCOPE: 16, CLAUSE: 3\n\nT244 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: mult(T255, s(s(s(0))), s(s(s(0))), T257)\n\nT255 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: mult(T267, s(s(s(s(T269)))), T269, T271)\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 1 | mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 2 | mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 3\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 1\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 2 | mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 3\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 2\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: mult(T267, s(s(s(s(T269)))), T269, T271), SCOPE: 17, CLAUSE: 3\n\nT267 is ground\nT269 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="E: mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294)\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 1 | mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 2 | mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 3\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 2 | mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 3\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: mult(T291, s(s(s(s(0)))), s(s(s(s(0)))), T294), SCOPE: 18, CLAUSE: 3\n\nT291 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: mult(T300, s(s(s(s(0)))), s(s(s(0))), T302)\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 1 | mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 2 | mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 3\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 2 | mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 3\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: mult(T300, s(s(s(s(0)))), s(s(s(0))), T302), SCOPE: 19, CLAUSE: 3\n\nT300 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: mult(T308, s(s(s(s(0)))), s(s(0)), T310)\n\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 1 | mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 2 | mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 3\n\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 2 | mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 3\n\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: mult(T308, s(s(s(s(0)))), s(s(0)), T310), SCOPE: 20, CLAUSE: 3\n\nT308 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: mult(T316, s(s(s(s(0)))), s(0), T318)\n\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 1 | mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 2 | mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 3\n\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 2 | mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 3\n\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: mult(T316, s(s(s(s(0)))), s(0), T318), SCOPE: 21, CLAUSE: 3\n\nT316 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: mult(T324, s(s(s(s(0)))), 0, T326)\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 1 | mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 2 | mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 3\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 1\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 2 | mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 3\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 2\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: mult(T324, s(s(s(s(0)))), 0, T326), SCOPE: 22, CLAUSE: 3\n\nT324 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: mult(T335, s(s(s(s(0)))), s(s(s(s(0)))), T337)\n\nT335 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: mult(T347, s(s(s(s(s(T349))))), T349, T351)\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 1 | mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 2 | mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 3\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 1\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 2 | mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 3\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 2\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: mult(T347, s(s(s(s(s(T349))))), T349, T351), SCOPE: 23, CLAUSE: 3\n\nT347 is ground\nT349 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="F: mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374)\n\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 1 | mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 2 | mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 3\n\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 2 | mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 3\n\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: mult(T371, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T374), SCOPE: 24, CLAUSE: 3\n\nT371 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382)\n\nT380 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 1 | mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 2 | mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 3\n\nT380 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 2 | mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 3\n\nT380 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: mult(T380, s(s(s(s(s(0))))), s(s(s(s(0)))), T382), SCOPE: 25, CLAUSE: 3\n\nT380 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390)\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 1 | mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 2 | mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 3\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 2 | mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 3\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: mult(T388, s(s(s(s(s(0))))), s(s(s(0))), T390), SCOPE: 26, CLAUSE: 3\n\nT388 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: mult(T396, s(s(s(s(s(0))))), s(s(0)), T398)\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 1 | mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 2 | mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 3\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 2 | mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 3\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: mult(T396, s(s(s(s(s(0))))), s(s(0)), T398), SCOPE: 27, CLAUSE: 3\n\nT396 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: mult(T404, s(s(s(s(s(0))))), s(0), T406)\n\nT404 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 1 | mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 2 | mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 3\n\nT404 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 2 | mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 3\n\nT404 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: mult(T404, s(s(s(s(s(0))))), s(0), T406), SCOPE: 28, CLAUSE: 3\n\nT404 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: mult(T412, s(s(s(s(s(0))))), 0, T414)\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 1 | mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 2 | mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 3\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 1\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 2 | mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 3\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 2\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: mult(T412, s(s(s(s(s(0))))), 0, T414), SCOPE: 29, CLAUSE: 3\n\nT412 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: mult(T423, s(s(s(s(s(0))))), s(s(s(s(s(0))))), T425)\n\nT423 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439)\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 1 | mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 2 | mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 3\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 1\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 2 | mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 3\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 2\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: mult(T435, s(s(s(s(s(s(T437)))))), T437, T439), SCOPE: 30, CLAUSE: 3\n\nT435 is ground\nT437 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="G: mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462)\n\nT459 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 1 | mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 2 | mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 3\n\nT459 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 2 | mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 3\n\nT459 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: mult(T459, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T462), SCOPE: 31, CLAUSE: 3\n\nT459 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470)\n\nT468 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 1 | mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 2 | mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 3\n\nT468 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 2 | mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 3\n\nT468 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: mult(T468, s(s(s(s(s(s(0)))))), s(s(s(s(s(0))))), T470), SCOPE: 32, CLAUSE: 3\n\nT468 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478)\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
246 [label="246: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 1 | mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 2 | mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 2 | mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: mult(T476, s(s(s(s(s(s(0)))))), s(s(s(s(0)))), T478), SCOPE: 33, CLAUSE: 3\n\nT476 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="250: mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486)\n\nT484 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
252 [label="252: mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 1 | mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 2 | mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 3\n\nT484 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 2 | mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 3\n\nT484 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: mult(T484, s(s(s(s(s(s(0)))))), s(s(s(0))), T486), SCOPE: 34, CLAUSE: 3\n\nT484 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494)\n\nT492 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 1 | mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 2 | mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 3\n\nT492 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 2 | mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 3\n\nT492 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: mult(T492, s(s(s(s(s(s(0)))))), s(s(0)), T494), SCOPE: 35, CLAUSE: 3\n\nT492 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: mult(T500, s(s(s(s(s(s(0)))))), s(0), T502)\n\nT500 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 1 | mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 2 | mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 3\n\nT500 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 2 | mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 3\n\nT500 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: mult(T500, s(s(s(s(s(s(0)))))), s(0), T502), SCOPE: 36, CLAUSE: 3\n\nT500 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: mult(T508, s(s(s(s(s(s(0)))))), 0, T510)\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 1 | mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 2 | mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 3\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 1\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 2 | mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 3\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 2\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: mult(T508, s(s(s(s(s(s(0)))))), 0, T510), SCOPE: 37, CLAUSE: 3\n\nT508 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: mult(T519, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0)))))), T521)\n\nT519 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="277: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
278 [label="278: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535)\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
279 [label="279: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
280 [label="280: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 1 | mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 2 | mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 3\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
281 [label="281: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 1\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
282 [label="282: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 2 | mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 3\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
283 [label="283: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
284 [label="284: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
285 [label="285: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 2\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: mult(T531, s(s(s(s(s(s(s(T533))))))), T533, T535), SCOPE: 38, CLAUSE: 3\n\nT531 is ground\nT533 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
288 [label="H: mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558)\n\nT555 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
290 [label="290: mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 1 | mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 2 | mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 3\n\nT555 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
291 [label="291: mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 2 | mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 3\n\nT555 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
292 [label="292: mult(T555, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T558), SCOPE: 39, CLAUSE: 3\n\nT555 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566)\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 1 | mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 2 | mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
296 [label="296: mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 2 | mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: mult(T564, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(0)))))), T566), SCOPE: 40, CLAUSE: 3\n\nT564 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574)\n\nT572 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
299 [label="299: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
300 [label="300: mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 1 | mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 2 | mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 3\n\nT572 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
301 [label="301: mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 2 | mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 3\n\nT572 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
302 [label="302: mult(T572, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(0))))), T574), SCOPE: 41, CLAUSE: 3\n\nT572 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
303 [label="303: mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582)\n\nT580 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
304 [label="304: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="305: mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 1 | mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 2 | mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 3\n\nT580 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 2 | mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 3\n\nT580 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
307 [label="307: mult(T580, s(s(s(s(s(s(s(0))))))), s(s(s(s(0)))), T582), SCOPE: 42, CLAUSE: 3\n\nT580 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
308 [label="308: mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590)\n\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
309 [label="309: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
310 [label="310: mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 1 | mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 2 | mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 3\n\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
311 [label="311: mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 2 | mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 3\n\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
312 [label="312: mult(T588, s(s(s(s(s(s(s(0))))))), s(s(s(0))), T590), SCOPE: 43, CLAUSE: 3\n\nT588 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
313 [label="313: mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598)\n\nT596 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
314 [label="314: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
315 [label="315: mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 1 | mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 2 | mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 3\n\nT596 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
316 [label="316: mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 2 | mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 3\n\nT596 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
317 [label="317: mult(T596, s(s(s(s(s(s(s(0))))))), s(s(0)), T598), SCOPE: 44, CLAUSE: 3\n\nT596 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
318 [label="318: mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606)\n\nT604 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
319 [label="319: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
320 [label="320: mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 1 | mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 2 | mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 3\n\nT604 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
321 [label="321: mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 2 | mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 3\n\nT604 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
322 [label="322: mult(T604, s(s(s(s(s(s(s(0))))))), s(0), T606), SCOPE: 45, CLAUSE: 3\n\nT604 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
323 [label="323: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614)\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
324 [label="324: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 1 | mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 2 | mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 3\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="326: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 1\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
327 [label="327: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 2 | mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 3\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
328 [label="328: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
329 [label="329: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
331 [label="331: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 2\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
332 [label="332: mult(T612, s(s(s(s(s(s(s(0))))))), 0, T614), SCOPE: 46, CLAUSE: 3\n\nT612 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
333 [label="333: mult(T623, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0))))))), T625)\n\nT623 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
334 [label="334: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: mult(T635, s(s(s(s(s(s(s(s(T637)))))))), T637, T639)\n\nT635 is ground\nT637 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
337 [label="337: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
338 [label="J: mult(T635, s(T642), T637, T639)\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
339 [label="339: mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 1 | mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 2 | mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 3\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 1\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 2 | mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 3\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
343 [label="343: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
344 [label="344: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
345 [label="345: mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 2\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
346 [label="346: mult(T635, s(T642), T637, T639), SCOPE: 47, CLAUSE: 3\n\nT635 is ground\nT637 is ground\nT642 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
347 [label="347: mult(T662, s(T663), s(T663), T665)\n\nT662 is ground\nT663 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
348 [label="348: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
349 [label="349: mult(T676, s(T677), T678, T680)\n\nT676 is ground\nT677 is ground\nT678 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
350 [label="350: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
351 [label="351: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
352 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 352 [arrowhead = none ];
352 -> 2;

353 [label="ONLY EVAL with clause\ntimes(X4, X5, X6) :- mult(X4, X5, 0, X6).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T8,\nX5 -> T8,\nT3 -> T10,\nX6 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 353 [arrowhead = none ];
353 -> 3;

354 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 354 [arrowhead = none ];
354 -> 4;

355 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 355 [arrowhead = none ];
355 -> 5;

356 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 356 [arrowhead = none ];
356 -> 6;

357 [label="EVAL with clause\nmult(0, X11, 0, 0).\nand substitutionT7 -> 0,\nT8 -> T15,\nX11 -> T15,\nT10 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 357 [arrowhead = none ];
357 -> 7;

358 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 358 [arrowhead = none ];
358 -> 8;

359 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 359 [arrowhead = none ];
359 -> 10;

360 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 360 [arrowhead = none ];
360 -> 11;

361 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 361 [arrowhead = none ];
361 -> 9;

362 [label="EVAL with clause\nmult(s(X24), X25, 0, X26) :- mult(X24, X25, X25, X26).\nand substitutionX24 -> T28,\nT7 -> s(T28),\nT8 -> T29,\nX25 -> T29,\nT10 -> T31,\nX26 -> T31,\nT30 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 362 [arrowhead = none ];
362 -> 12;

363 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 363 [arrowhead = none ];
363 -> 13;

364 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 364 [arrowhead = none ];
364 -> 351;

365 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 365 [arrowhead = none ];
365 -> 14;

366 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 366 [arrowhead = none ];
366 -> 15;

367 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 367 [arrowhead = none ];
367 -> 16;

368 [label="EVAL with clause\nmult(0, X33, 0, 0).\nand substitutionT28 -> 0,\nT29 -> 0,\nX33 -> 0,\nT38 -> 0,\nT31 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 368 [arrowhead = none ];
368 -> 17;

369 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 369 [arrowhead = none ];
369 -> 18;

370 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 370 [arrowhead = none ];
370 -> 20;

371 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
16 -> 371 [arrowhead = none ];
371 -> 21;

372 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 372 [arrowhead = none ];
372 -> 19;

373 [label="EVAL with clause\nmult(s(X46), X47, 0, X48) :- mult(X46, X47, X47, X48).\nand substitutionX46 -> T51,\nT28 -> s(T51),\nT29 -> 0,\nX47 -> 0,\nT52 -> 0,\nT31 -> T54,\nX48 -> T54,\nT53 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 373 [arrowhead = none ];
373 -> 22;

374 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 374 [arrowhead = none ];
374 -> 23;

375 [label="EVAL with clause\nmult(X85, X86, s(X87), s(X88)) :- mult(X85, X86, X87, X88).\nand substitutionT28 -> T75,\nX85 -> T75,\nT29 -> s(T77),\nX86 -> s(T77),\nX87 -> T77,\nT76 -> s(T77),\nX88 -> T79,\nT31 -> s(T79),\nT78 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 375 [arrowhead = none ];
375 -> 35;

376 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 376 [arrowhead = none ];
376 -> 36;

377 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
22 -> 377 [arrowhead = none ];
377 -> 24;

378 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 378 [arrowhead = none ];
378 -> 25;

379 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
24 -> 379 [arrowhead = none ];
379 -> 26;

380 [label="EVAL with clause\nmult(0, X55, 0, 0).\nand substitutionT51 -> 0,\nX55 -> 0,\nT54 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 380 [arrowhead = none ];
380 -> 27;

381 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 381 [arrowhead = none ];
381 -> 28;

382 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 382 [arrowhead = none ];
382 -> 30;

383 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 383 [arrowhead = none ];
383 -> 31;

384 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 384 [arrowhead = none ];
384 -> 29;

385 [label="EVAL with clause\nmult(s(X68), X69, 0, X70) :- mult(X68, X69, X69, X70).\nand substitutionX68 -> T63,\nT51 -> s(T63),\nX69 -> 0,\nT54 -> T65,\nX70 -> T65,\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 385 [arrowhead = none ];
385 -> 32;

386 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 386 [arrowhead = none ];
386 -> 33;

387 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 387 [arrowhead = none ];
387 -> 34;

388 [label="INSTANCE with matching:\nT51 -> T63\nT54 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 388 [arrowhead = none , style=dashed];
388 -> 22[style=dashed];

389 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 389 [arrowhead = none ];
389 -> 37;

390 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 390 [arrowhead = none ];
390 -> 38;

391 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 391 [arrowhead = none ];
391 -> 39;

392 [label="EVAL with clause\nmult(0, X95, 0, 0).\nand substitutionT75 -> 0,\nT77 -> 0,\nX95 -> s(0),\nT86 -> 0,\nT79 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 392 [arrowhead = none ];
392 -> 40;

393 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 393 [arrowhead = none ];
393 -> 41;

394 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 394 [arrowhead = none ];
394 -> 43;

395 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 395 [arrowhead = none ];
395 -> 44;

396 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 396 [arrowhead = none ];
396 -> 42;

397 [label="EVAL with clause\nmult(s(X108), X109, 0, X110) :- mult(X108, X109, X109, X110).\nand substitutionX108 -> T99,\nT75 -> s(T99),\nT77 -> 0,\nX109 -> s(0),\nT100 -> 0,\nT79 -> T102,\nX110 -> T102,\nT101 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 397 [arrowhead = none ];
397 -> 45;

398 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
43 -> 398 [arrowhead = none ];
398 -> 46;

399 [label="EVAL with clause\nmult(X165, X166, s(X167), s(X168)) :- mult(X165, X166, X167, X168).\nand substitutionT75 -> T131,\nX165 -> T131,\nT77 -> s(T133),\nX166 -> s(s(T133)),\nX167 -> T133,\nT132 -> s(T133),\nX168 -> T135,\nT79 -> s(T135),\nT134 -> T135", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 399 [arrowhead = none ];
399 -> 63;

400 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 400 [arrowhead = none ];
400 -> 64;

401 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 401 [arrowhead = none ];
401 -> 47;

402 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 402 [arrowhead = none ];
402 -> 48;

403 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 403 [arrowhead = none ];
403 -> 49;

404 [label="EVAL with clause\nmult(X125, X126, s(X127), s(X128)) :- mult(X125, X126, X127, X128).\nand substitutionT99 -> T108,\nX125 -> T108,\nX126 -> s(0),\nX127 -> 0,\nX128 -> T110,\nT102 -> s(T110),\nT109 -> T110", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 404 [arrowhead = none ];
404 -> 50;

405 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 405 [arrowhead = none ];
405 -> 51;

406 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 406 [arrowhead = none ];
406 -> 52;

407 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 407 [arrowhead = none ];
407 -> 53;

408 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 408 [arrowhead = none ];
408 -> 54;

409 [label="EVAL with clause\nmult(0, X135, 0, 0).\nand substitutionT108 -> 0,\nX135 -> s(0),\nT110 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 409 [arrowhead = none ];
409 -> 55;

410 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 410 [arrowhead = none ];
410 -> 56;

411 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 411 [arrowhead = none ];
411 -> 58;

412 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
54 -> 412 [arrowhead = none ];
412 -> 59;

413 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 413 [arrowhead = none ];
413 -> 57;

414 [label="EVAL with clause\nmult(s(X148), X149, 0, X150) :- mult(X148, X149, X149, X150).\nand substitutionX148 -> T119,\nT108 -> s(T119),\nX149 -> s(0),\nT110 -> T121,\nX150 -> T121,\nT120 -> T121", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 414 [arrowhead = none ];
414 -> 60;

415 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 415 [arrowhead = none ];
415 -> 61;

416 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 416 [arrowhead = none ];
416 -> 62;

417 [label="INSTANCE with matching:\nT99 -> T119\nT102 -> T121", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 417 [arrowhead = none , style=dashed];
417 -> 45[style=dashed];

418 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 418 [arrowhead = none ];
418 -> 65;

419 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 419 [arrowhead = none ];
419 -> 66;

420 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 420 [arrowhead = none ];
420 -> 67;

421 [label="EVAL with clause\nmult(0, X175, 0, 0).\nand substitutionT131 -> 0,\nT133 -> 0,\nX175 -> s(s(0)),\nT142 -> 0,\nT135 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 421 [arrowhead = none ];
421 -> 68;

422 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 422 [arrowhead = none ];
422 -> 69;

423 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 423 [arrowhead = none ];
423 -> 71;

424 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
67 -> 424 [arrowhead = none ];
424 -> 72;

425 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 425 [arrowhead = none ];
425 -> 70;

426 [label="EVAL with clause\nmult(s(X188), X189, 0, X190) :- mult(X188, X189, X189, X190).\nand substitutionX188 -> T155,\nT131 -> s(T155),\nT133 -> 0,\nX189 -> s(s(0)),\nT156 -> 0,\nT135 -> T158,\nX190 -> T158,\nT157 -> T158", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 426 [arrowhead = none ];
426 -> 73;

427 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 427 [arrowhead = none ];
427 -> 74;

428 [label="EVAL with clause\nmult(X263, X264, s(X265), s(X266)) :- mult(X263, X264, X265, X266).\nand substitutionT131 -> T195,\nX263 -> T195,\nT133 -> s(T197),\nX264 -> s(s(s(T197))),\nX265 -> T197,\nT196 -> s(T197),\nX266 -> T199,\nT135 -> s(T199),\nT198 -> T199", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 428 [arrowhead = none ];
428 -> 96;

429 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 429 [arrowhead = none ];
429 -> 97;

430 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 430 [arrowhead = none ];
430 -> 75;

431 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
75 -> 431 [arrowhead = none ];
431 -> 76;

432 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 432 [arrowhead = none ];
432 -> 77;

433 [label="EVAL with clause\nmult(X205, X206, s(X207), s(X208)) :- mult(X205, X206, X207, X208).\nand substitutionT155 -> T164,\nX205 -> T164,\nX206 -> s(s(0)),\nX207 -> s(0),\nX208 -> T166,\nT158 -> s(T166),\nT165 -> T166", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 433 [arrowhead = none ];
433 -> 78;

434 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 434 [arrowhead = none ];
434 -> 79;

435 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
78 -> 435 [arrowhead = none ];
435 -> 80;

436 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 436 [arrowhead = none ];
436 -> 81;

437 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 437 [arrowhead = none ];
437 -> 82;

438 [label="EVAL with clause\nmult(X223, X224, s(X225), s(X226)) :- mult(X223, X224, X225, X226).\nand substitutionT164 -> T172,\nX223 -> T172,\nX224 -> s(s(0)),\nX225 -> 0,\nX226 -> T174,\nT166 -> s(T174),\nT173 -> T174", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 438 [arrowhead = none ];
438 -> 83;

439 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 439 [arrowhead = none ];
439 -> 84;

440 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
83 -> 440 [arrowhead = none ];
440 -> 85;

441 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 441 [arrowhead = none ];
441 -> 86;

442 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
85 -> 442 [arrowhead = none ];
442 -> 87;

443 [label="EVAL with clause\nmult(0, X233, 0, 0).\nand substitutionT172 -> 0,\nX233 -> s(s(0)),\nT174 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 443 [arrowhead = none ];
443 -> 88;

444 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
86 -> 444 [arrowhead = none ];
444 -> 89;

445 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 445 [arrowhead = none ];
445 -> 91;

446 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
87 -> 446 [arrowhead = none ];
446 -> 92;

447 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 447 [arrowhead = none ];
447 -> 90;

448 [label="EVAL with clause\nmult(s(X246), X247, 0, X248) :- mult(X246, X247, X247, X248).\nand substitutionX246 -> T183,\nT172 -> s(T183),\nX247 -> s(s(0)),\nT174 -> T185,\nX248 -> T185,\nT184 -> T185", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 448 [arrowhead = none ];
448 -> 93;

449 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 449 [arrowhead = none ];
449 -> 94;

450 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 450 [arrowhead = none ];
450 -> 95;

451 [label="INSTANCE with matching:\nT155 -> T183\nT158 -> T185", fontsize=14, style = filled, fillcolor = lightgrey];
93 -> 451 [arrowhead = none , style=dashed];
451 -> 73[style=dashed];

452 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 452 [arrowhead = none ];
452 -> 98;

453 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 453 [arrowhead = none ];
453 -> 99;

454 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 454 [arrowhead = none ];
454 -> 100;

455 [label="EVAL with clause\nmult(0, X273, 0, 0).\nand substitutionT195 -> 0,\nT197 -> 0,\nX273 -> s(s(s(0))),\nT206 -> 0,\nT199 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 455 [arrowhead = none ];
455 -> 101;

456 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 456 [arrowhead = none ];
456 -> 102;

457 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 457 [arrowhead = none ];
457 -> 104;

458 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 458 [arrowhead = none ];
458 -> 105;

459 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 459 [arrowhead = none ];
459 -> 103;

460 [label="EVAL with clause\nmult(s(X286), X287, 0, X288) :- mult(X286, X287, X287, X288).\nand substitutionX286 -> T219,\nT195 -> s(T219),\nT197 -> 0,\nX287 -> s(s(s(0))),\nT220 -> 0,\nT199 -> T222,\nX288 -> T222,\nT221 -> T222", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 460 [arrowhead = none ];
460 -> 106;

461 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 461 [arrowhead = none ];
461 -> 107;

462 [label="EVAL with clause\nmult(X379, X380, s(X381), s(X382)) :- mult(X379, X380, X381, X382).\nand substitutionT195 -> T267,\nX379 -> T267,\nT197 -> s(T269),\nX380 -> s(s(s(s(T269)))),\nX381 -> T269,\nT268 -> s(T269),\nX382 -> T271,\nT199 -> s(T271),\nT270 -> T271", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 462 [arrowhead = none ];
462 -> 134;

463 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 463 [arrowhead = none ];
463 -> 135;

464 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
106 -> 464 [arrowhead = none ];
464 -> 108;

465 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 465 [arrowhead = none ];
465 -> 109;

466 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
109 -> 466 [arrowhead = none ];
466 -> 110;

467 [label="EVAL with clause\nmult(X303, X304, s(X305), s(X306)) :- mult(X303, X304, X305, X306).\nand substitutionT219 -> T228,\nX303 -> T228,\nX304 -> s(s(s(0))),\nX305 -> s(s(0)),\nX306 -> T230,\nT222 -> s(T230),\nT229 -> T230", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 467 [arrowhead = none ];
467 -> 111;

468 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 468 [arrowhead = none ];
468 -> 112;

469 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
111 -> 469 [arrowhead = none ];
469 -> 113;

470 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 470 [arrowhead = none ];
470 -> 114;

471 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 471 [arrowhead = none ];
471 -> 115;

472 [label="EVAL with clause\nmult(X321, X322, s(X323), s(X324)) :- mult(X321, X322, X323, X324).\nand substitutionT228 -> T236,\nX321 -> T236,\nX322 -> s(s(s(0))),\nX323 -> s(0),\nX324 -> T238,\nT230 -> s(T238),\nT237 -> T238", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 472 [arrowhead = none ];
472 -> 116;

473 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
115 -> 473 [arrowhead = none ];
473 -> 117;

474 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
116 -> 474 [arrowhead = none ];
474 -> 118;

475 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 475 [arrowhead = none ];
475 -> 119;

476 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 476 [arrowhead = none ];
476 -> 120;

477 [label="EVAL with clause\nmult(X339, X340, s(X341), s(X342)) :- mult(X339, X340, X341, X342).\nand substitutionT236 -> T244,\nX339 -> T244,\nX340 -> s(s(s(0))),\nX341 -> 0,\nX342 -> T246,\nT238 -> s(T246),\nT245 -> T246", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 477 [arrowhead = none ];
477 -> 121;

478 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 478 [arrowhead = none ];
478 -> 122;

479 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
121 -> 479 [arrowhead = none ];
479 -> 123;

480 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 480 [arrowhead = none ];
480 -> 124;

481 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 481 [arrowhead = none ];
481 -> 125;

482 [label="EVAL with clause\nmult(0, X349, 0, 0).\nand substitutionT244 -> 0,\nX349 -> s(s(s(0))),\nT246 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 482 [arrowhead = none ];
482 -> 126;

483 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 483 [arrowhead = none ];
483 -> 127;

484 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 484 [arrowhead = none ];
484 -> 129;

485 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 485 [arrowhead = none ];
485 -> 130;

486 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 486 [arrowhead = none ];
486 -> 128;

487 [label="EVAL with clause\nmult(s(X362), X363, 0, X364) :- mult(X362, X363, X363, X364).\nand substitutionX362 -> T255,\nT244 -> s(T255),\nX363 -> s(s(s(0))),\nT246 -> T257,\nX364 -> T257,\nT256 -> T257", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 487 [arrowhead = none ];
487 -> 131;

488 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 488 [arrowhead = none ];
488 -> 132;

489 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
130 -> 489 [arrowhead = none ];
489 -> 133;

490 [label="INSTANCE with matching:\nT219 -> T255\nT222 -> T257", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 490 [arrowhead = none , style=dashed];
490 -> 106[style=dashed];

491 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
134 -> 491 [arrowhead = none ];
491 -> 136;

492 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 492 [arrowhead = none ];
492 -> 137;

493 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
136 -> 493 [arrowhead = none ];
493 -> 138;

494 [label="EVAL with clause\nmult(0, X389, 0, 0).\nand substitutionT267 -> 0,\nT269 -> 0,\nX389 -> s(s(s(s(0)))),\nT278 -> 0,\nT271 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 494 [arrowhead = none ];
494 -> 139;

495 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 495 [arrowhead = none ];
495 -> 140;

496 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 496 [arrowhead = none ];
496 -> 142;

497 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
138 -> 497 [arrowhead = none ];
497 -> 143;

498 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
139 -> 498 [arrowhead = none ];
498 -> 141;

499 [label="EVAL with clause\nmult(s(X402), X403, 0, X404) :- mult(X402, X403, X403, X404).\nand substitutionX402 -> T291,\nT267 -> s(T291),\nT269 -> 0,\nX403 -> s(s(s(s(0)))),\nT292 -> 0,\nT271 -> T294,\nX404 -> T294,\nT293 -> T294", fontsize=14, style = filled, fillcolor = lightblue];
142 -> 499 [arrowhead = none ];
499 -> 144;

500 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
142 -> 500 [arrowhead = none ];
500 -> 145;

501 [label="EVAL with clause\nmult(X513, X514, s(X515), s(X516)) :- mult(X513, X514, X515, X516).\nand substitutionT267 -> T347,\nX513 -> T347,\nT269 -> s(T349),\nX514 -> s(s(s(s(s(T349))))),\nX515 -> T349,\nT348 -> s(T349),\nX516 -> T351,\nT271 -> s(T351),\nT350 -> T351", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 501 [arrowhead = none ];
501 -> 177;

502 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 502 [arrowhead = none ];
502 -> 178;

503 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 503 [arrowhead = none ];
503 -> 146;

504 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
146 -> 504 [arrowhead = none ];
504 -> 147;

505 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 505 [arrowhead = none ];
505 -> 148;

506 [label="EVAL with clause\nmult(X419, X420, s(X421), s(X422)) :- mult(X419, X420, X421, X422).\nand substitutionT291 -> T300,\nX419 -> T300,\nX420 -> s(s(s(s(0)))),\nX421 -> s(s(s(0))),\nX422 -> T302,\nT294 -> s(T302),\nT301 -> T302", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 506 [arrowhead = none ];
506 -> 149;

507 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 507 [arrowhead = none ];
507 -> 150;

508 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
149 -> 508 [arrowhead = none ];
508 -> 151;

509 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
151 -> 509 [arrowhead = none ];
509 -> 152;

510 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 510 [arrowhead = none ];
510 -> 153;

511 [label="EVAL with clause\nmult(X437, X438, s(X439), s(X440)) :- mult(X437, X438, X439, X440).\nand substitutionT300 -> T308,\nX437 -> T308,\nX438 -> s(s(s(s(0)))),\nX439 -> s(s(0)),\nX440 -> T310,\nT302 -> s(T310),\nT309 -> T310", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 511 [arrowhead = none ];
511 -> 154;

512 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
153 -> 512 [arrowhead = none ];
512 -> 155;

513 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
154 -> 513 [arrowhead = none ];
513 -> 156;

514 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 514 [arrowhead = none ];
514 -> 157;

515 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 515 [arrowhead = none ];
515 -> 158;

516 [label="EVAL with clause\nmult(X455, X456, s(X457), s(X458)) :- mult(X455, X456, X457, X458).\nand substitutionT308 -> T316,\nX455 -> T316,\nX456 -> s(s(s(s(0)))),\nX457 -> s(0),\nX458 -> T318,\nT310 -> s(T318),\nT317 -> T318", fontsize=14, style = filled, fillcolor = lightblue];
158 -> 516 [arrowhead = none ];
516 -> 159;

517 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
158 -> 517 [arrowhead = none ];
517 -> 160;

518 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
159 -> 518 [arrowhead = none ];
518 -> 161;

519 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
161 -> 519 [arrowhead = none ];
519 -> 162;

520 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
162 -> 520 [arrowhead = none ];
520 -> 163;

521 [label="EVAL with clause\nmult(X473, X474, s(X475), s(X476)) :- mult(X473, X474, X475, X476).\nand substitutionT316 -> T324,\nX473 -> T324,\nX474 -> s(s(s(s(0)))),\nX475 -> 0,\nX476 -> T326,\nT318 -> s(T326),\nT325 -> T326", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 521 [arrowhead = none ];
521 -> 164;

522 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 522 [arrowhead = none ];
522 -> 165;

523 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 523 [arrowhead = none ];
523 -> 166;

524 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 524 [arrowhead = none ];
524 -> 167;

525 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
166 -> 525 [arrowhead = none ];
525 -> 168;

526 [label="EVAL with clause\nmult(0, X483, 0, 0).\nand substitutionT324 -> 0,\nX483 -> s(s(s(s(0)))),\nT326 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 526 [arrowhead = none ];
526 -> 169;

527 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
167 -> 527 [arrowhead = none ];
527 -> 170;

528 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 528 [arrowhead = none ];
528 -> 172;

529 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 529 [arrowhead = none ];
529 -> 173;

530 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
169 -> 530 [arrowhead = none ];
530 -> 171;

531 [label="EVAL with clause\nmult(s(X496), X497, 0, X498) :- mult(X496, X497, X497, X498).\nand substitutionX496 -> T335,\nT324 -> s(T335),\nX497 -> s(s(s(s(0)))),\nT326 -> T337,\nX498 -> T337,\nT336 -> T337", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 531 [arrowhead = none ];
531 -> 174;

532 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 532 [arrowhead = none ];
532 -> 175;

533 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 533 [arrowhead = none ];
533 -> 176;

534 [label="INSTANCE with matching:\nT291 -> T335\nT294 -> T337", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 534 [arrowhead = none , style=dashed];
534 -> 144[style=dashed];

535 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
177 -> 535 [arrowhead = none ];
535 -> 179;

536 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 536 [arrowhead = none ];
536 -> 180;

537 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 537 [arrowhead = none ];
537 -> 181;

538 [label="EVAL with clause\nmult(0, X523, 0, 0).\nand substitutionT347 -> 0,\nT349 -> 0,\nX523 -> s(s(s(s(s(0))))),\nT358 -> 0,\nT351 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
180 -> 538 [arrowhead = none ];
538 -> 182;

539 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
180 -> 539 [arrowhead = none ];
539 -> 183;

540 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 540 [arrowhead = none ];
540 -> 185;

541 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
181 -> 541 [arrowhead = none ];
541 -> 186;

542 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 542 [arrowhead = none ];
542 -> 184;

543 [label="EVAL with clause\nmult(s(X536), X537, 0, X538) :- mult(X536, X537, X537, X538).\nand substitutionX536 -> T371,\nT347 -> s(T371),\nT349 -> 0,\nX537 -> s(s(s(s(s(0))))),\nT372 -> 0,\nT351 -> T374,\nX538 -> T374,\nT373 -> T374", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 543 [arrowhead = none ];
543 -> 187;

544 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 544 [arrowhead = none ];
544 -> 188;

545 [label="EVAL with clause\nmult(X665, X666, s(X667), s(X668)) :- mult(X665, X666, X667, X668).\nand substitutionT347 -> T435,\nX665 -> T435,\nT349 -> s(T437),\nX666 -> s(s(s(s(s(s(T437)))))),\nX667 -> T437,\nT436 -> s(T437),\nX668 -> T439,\nT351 -> s(T439),\nT438 -> T439", fontsize=14, style = filled, fillcolor = lightblue];
186 -> 545 [arrowhead = none ];
545 -> 225;

546 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 546 [arrowhead = none ];
546 -> 226;

547 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
187 -> 547 [arrowhead = none ];
547 -> 189;

548 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
189 -> 548 [arrowhead = none ];
548 -> 190;

549 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
190 -> 549 [arrowhead = none ];
549 -> 191;

550 [label="EVAL with clause\nmult(X553, X554, s(X555), s(X556)) :- mult(X553, X554, X555, X556).\nand substitutionT371 -> T380,\nX553 -> T380,\nX554 -> s(s(s(s(s(0))))),\nX555 -> s(s(s(s(0)))),\nX556 -> T382,\nT374 -> s(T382),\nT381 -> T382", fontsize=14, style = filled, fillcolor = lightblue];
191 -> 550 [arrowhead = none ];
550 -> 192;

551 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
191 -> 551 [arrowhead = none ];
551 -> 193;

552 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
192 -> 552 [arrowhead = none ];
552 -> 194;

553 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
194 -> 553 [arrowhead = none ];
553 -> 195;

554 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 554 [arrowhead = none ];
554 -> 196;

555 [label="EVAL with clause\nmult(X571, X572, s(X573), s(X574)) :- mult(X571, X572, X573, X574).\nand substitutionT380 -> T388,\nX571 -> T388,\nX572 -> s(s(s(s(s(0))))),\nX573 -> s(s(s(0))),\nX574 -> T390,\nT382 -> s(T390),\nT389 -> T390", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 555 [arrowhead = none ];
555 -> 197;

556 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 556 [arrowhead = none ];
556 -> 198;

557 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
197 -> 557 [arrowhead = none ];
557 -> 199;

558 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
199 -> 558 [arrowhead = none ];
558 -> 200;

559 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 559 [arrowhead = none ];
559 -> 201;

560 [label="EVAL with clause\nmult(X589, X590, s(X591), s(X592)) :- mult(X589, X590, X591, X592).\nand substitutionT388 -> T396,\nX589 -> T396,\nX590 -> s(s(s(s(s(0))))),\nX591 -> s(s(0)),\nX592 -> T398,\nT390 -> s(T398),\nT397 -> T398", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 560 [arrowhead = none ];
560 -> 202;

561 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 561 [arrowhead = none ];
561 -> 203;

562 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
202 -> 562 [arrowhead = none ];
562 -> 204;

563 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
204 -> 563 [arrowhead = none ];
563 -> 205;

564 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 564 [arrowhead = none ];
564 -> 206;

565 [label="EVAL with clause\nmult(X607, X608, s(X609), s(X610)) :- mult(X607, X608, X609, X610).\nand substitutionT396 -> T404,\nX607 -> T404,\nX608 -> s(s(s(s(s(0))))),\nX609 -> s(0),\nX610 -> T406,\nT398 -> s(T406),\nT405 -> T406", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 565 [arrowhead = none ];
565 -> 207;

566 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 566 [arrowhead = none ];
566 -> 208;

567 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
207 -> 567 [arrowhead = none ];
567 -> 209;

568 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
209 -> 568 [arrowhead = none ];
568 -> 210;

569 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
210 -> 569 [arrowhead = none ];
569 -> 211;

570 [label="EVAL with clause\nmult(X625, X626, s(X627), s(X628)) :- mult(X625, X626, X627, X628).\nand substitutionT404 -> T412,\nX625 -> T412,\nX626 -> s(s(s(s(s(0))))),\nX627 -> 0,\nX628 -> T414,\nT406 -> s(T414),\nT413 -> T414", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 570 [arrowhead = none ];
570 -> 212;

571 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
211 -> 571 [arrowhead = none ];
571 -> 213;

572 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
212 -> 572 [arrowhead = none ];
572 -> 214;

573 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
214 -> 573 [arrowhead = none ];
573 -> 215;

574 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
214 -> 574 [arrowhead = none ];
574 -> 216;

575 [label="EVAL with clause\nmult(0, X635, 0, 0).\nand substitutionT412 -> 0,\nX635 -> s(s(s(s(s(0))))),\nT414 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 575 [arrowhead = none ];
575 -> 217;

576 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
215 -> 576 [arrowhead = none ];
576 -> 218;

577 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
216 -> 577 [arrowhead = none ];
577 -> 220;

578 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
216 -> 578 [arrowhead = none ];
578 -> 221;

579 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 579 [arrowhead = none ];
579 -> 219;

580 [label="EVAL with clause\nmult(s(X648), X649, 0, X650) :- mult(X648, X649, X649, X650).\nand substitutionX648 -> T423,\nT412 -> s(T423),\nX649 -> s(s(s(s(s(0))))),\nT414 -> T425,\nX650 -> T425,\nT424 -> T425", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 580 [arrowhead = none ];
580 -> 222;

581 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 581 [arrowhead = none ];
581 -> 223;

582 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 582 [arrowhead = none ];
582 -> 224;

583 [label="INSTANCE with matching:\nT371 -> T423\nT374 -> T425", fontsize=14, style = filled, fillcolor = lightgrey];
222 -> 583 [arrowhead = none , style=dashed];
583 -> 187[style=dashed];

584 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
225 -> 584 [arrowhead = none ];
584 -> 227;

585 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 585 [arrowhead = none ];
585 -> 228;

586 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
227 -> 586 [arrowhead = none ];
586 -> 229;

587 [label="EVAL with clause\nmult(0, X675, 0, 0).\nand substitutionT435 -> 0,\nT437 -> 0,\nX675 -> s(s(s(s(s(s(0)))))),\nT446 -> 0,\nT439 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 587 [arrowhead = none ];
587 -> 230;

588 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
228 -> 588 [arrowhead = none ];
588 -> 231;

589 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
229 -> 589 [arrowhead = none ];
589 -> 233;

590 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
229 -> 590 [arrowhead = none ];
590 -> 234;

591 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
230 -> 591 [arrowhead = none ];
591 -> 232;

592 [label="EVAL with clause\nmult(s(X688), X689, 0, X690) :- mult(X688, X689, X689, X690).\nand substitutionX688 -> T459,\nT435 -> s(T459),\nT437 -> 0,\nX689 -> s(s(s(s(s(s(0)))))),\nT460 -> 0,\nT439 -> T462,\nX690 -> T462,\nT461 -> T462", fontsize=14, style = filled, fillcolor = lightblue];
233 -> 592 [arrowhead = none ];
592 -> 235;

593 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
233 -> 593 [arrowhead = none ];
593 -> 236;

594 [label="EVAL with clause\nmult(X835, X836, s(X837), s(X838)) :- mult(X835, X836, X837, X838).\nand substitutionT435 -> T531,\nX835 -> T531,\nT437 -> s(T533),\nX836 -> s(s(s(s(s(s(s(T533))))))),\nX837 -> T533,\nT532 -> s(T533),\nX838 -> T535,\nT439 -> s(T535),\nT534 -> T535", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 594 [arrowhead = none ];
594 -> 278;

595 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
234 -> 595 [arrowhead = none ];
595 -> 279;

596 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
235 -> 596 [arrowhead = none ];
596 -> 237;

597 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 597 [arrowhead = none ];
597 -> 238;

598 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 598 [arrowhead = none ];
598 -> 239;

599 [label="EVAL with clause\nmult(X705, X706, s(X707), s(X708)) :- mult(X705, X706, X707, X708).\nand substitutionT459 -> T468,\nX705 -> T468,\nX706 -> s(s(s(s(s(s(0)))))),\nX707 -> s(s(s(s(s(0))))),\nX708 -> T470,\nT462 -> s(T470),\nT469 -> T470", fontsize=14, style = filled, fillcolor = lightblue];
239 -> 599 [arrowhead = none ];
599 -> 240;

600 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
239 -> 600 [arrowhead = none ];
600 -> 241;

601 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
240 -> 601 [arrowhead = none ];
601 -> 242;

602 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
242 -> 602 [arrowhead = none ];
602 -> 243;

603 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
243 -> 603 [arrowhead = none ];
603 -> 244;

604 [label="EVAL with clause\nmult(X723, X724, s(X725), s(X726)) :- mult(X723, X724, X725, X726).\nand substitutionT468 -> T476,\nX723 -> T476,\nX724 -> s(s(s(s(s(s(0)))))),\nX725 -> s(s(s(s(0)))),\nX726 -> T478,\nT470 -> s(T478),\nT477 -> T478", fontsize=14, style = filled, fillcolor = lightblue];
244 -> 604 [arrowhead = none ];
604 -> 245;

605 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
244 -> 605 [arrowhead = none ];
605 -> 246;

606 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
245 -> 606 [arrowhead = none ];
606 -> 247;

607 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
247 -> 607 [arrowhead = none ];
607 -> 248;

608 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
248 -> 608 [arrowhead = none ];
608 -> 249;

609 [label="EVAL with clause\nmult(X741, X742, s(X743), s(X744)) :- mult(X741, X742, X743, X744).\nand substitutionT476 -> T484,\nX741 -> T484,\nX742 -> s(s(s(s(s(s(0)))))),\nX743 -> s(s(s(0))),\nX744 -> T486,\nT478 -> s(T486),\nT485 -> T486", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 609 [arrowhead = none ];
609 -> 250;

610 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
249 -> 610 [arrowhead = none ];
610 -> 251;

611 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
250 -> 611 [arrowhead = none ];
611 -> 252;

612 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
252 -> 612 [arrowhead = none ];
612 -> 253;

613 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
253 -> 613 [arrowhead = none ];
613 -> 254;

614 [label="EVAL with clause\nmult(X759, X760, s(X761), s(X762)) :- mult(X759, X760, X761, X762).\nand substitutionT484 -> T492,\nX759 -> T492,\nX760 -> s(s(s(s(s(s(0)))))),\nX761 -> s(s(0)),\nX762 -> T494,\nT486 -> s(T494),\nT493 -> T494", fontsize=14, style = filled, fillcolor = lightblue];
254 -> 614 [arrowhead = none ];
614 -> 255;

615 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
254 -> 615 [arrowhead = none ];
615 -> 256;

616 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
255 -> 616 [arrowhead = none ];
616 -> 257;

617 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
257 -> 617 [arrowhead = none ];
617 -> 258;

618 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
258 -> 618 [arrowhead = none ];
618 -> 259;

619 [label="EVAL with clause\nmult(X777, X778, s(X779), s(X780)) :- mult(X777, X778, X779, X780).\nand substitutionT492 -> T500,\nX777 -> T500,\nX778 -> s(s(s(s(s(s(0)))))),\nX779 -> s(0),\nX780 -> T502,\nT494 -> s(T502),\nT501 -> T502", fontsize=14, style = filled, fillcolor = lightblue];
259 -> 619 [arrowhead = none ];
619 -> 260;

620 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
259 -> 620 [arrowhead = none ];
620 -> 261;

621 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
260 -> 621 [arrowhead = none ];
621 -> 262;

622 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 622 [arrowhead = none ];
622 -> 263;

623 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 623 [arrowhead = none ];
623 -> 264;

624 [label="EVAL with clause\nmult(X795, X796, s(X797), s(X798)) :- mult(X795, X796, X797, X798).\nand substitutionT500 -> T508,\nX795 -> T508,\nX796 -> s(s(s(s(s(s(0)))))),\nX797 -> 0,\nX798 -> T510,\nT502 -> s(T510),\nT509 -> T510", fontsize=14, style = filled, fillcolor = lightblue];
264 -> 624 [arrowhead = none ];
624 -> 265;

625 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
264 -> 625 [arrowhead = none ];
625 -> 266;

626 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
265 -> 626 [arrowhead = none ];
626 -> 267;

627 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
267 -> 627 [arrowhead = none ];
627 -> 268;

628 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
267 -> 628 [arrowhead = none ];
628 -> 269;

629 [label="EVAL with clause\nmult(0, X805, 0, 0).\nand substitutionT508 -> 0,\nX805 -> s(s(s(s(s(s(0)))))),\nT510 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
268 -> 629 [arrowhead = none ];
629 -> 270;

630 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
268 -> 630 [arrowhead = none ];
630 -> 271;

631 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
269 -> 631 [arrowhead = none ];
631 -> 273;

632 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
269 -> 632 [arrowhead = none ];
632 -> 274;

633 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
270 -> 633 [arrowhead = none ];
633 -> 272;

634 [label="EVAL with clause\nmult(s(X818), X819, 0, X820) :- mult(X818, X819, X819, X820).\nand substitutionX818 -> T519,\nT508 -> s(T519),\nX819 -> s(s(s(s(s(s(0)))))),\nT510 -> T521,\nX820 -> T521,\nT520 -> T521", fontsize=14, style = filled, fillcolor = lightblue];
273 -> 634 [arrowhead = none ];
634 -> 275;

635 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
273 -> 635 [arrowhead = none ];
635 -> 276;

636 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
274 -> 636 [arrowhead = none ];
636 -> 277;

637 [label="INSTANCE with matching:\nT459 -> T519\nT462 -> T521", fontsize=14, style = filled, fillcolor = lightgrey];
275 -> 637 [arrowhead = none , style=dashed];
637 -> 235[style=dashed];

638 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
278 -> 638 [arrowhead = none ];
638 -> 280;

639 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 639 [arrowhead = none ];
639 -> 281;

640 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
280 -> 640 [arrowhead = none ];
640 -> 282;

641 [label="EVAL with clause\nmult(0, X845, 0, 0).\nand substitutionT531 -> 0,\nT533 -> 0,\nX845 -> s(s(s(s(s(s(s(0))))))),\nT542 -> 0,\nT535 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
281 -> 641 [arrowhead = none ];
641 -> 283;

642 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
281 -> 642 [arrowhead = none ];
642 -> 284;

643 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 643 [arrowhead = none ];
643 -> 286;

644 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
282 -> 644 [arrowhead = none ];
644 -> 287;

645 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
283 -> 645 [arrowhead = none ];
645 -> 285;

646 [label="EVAL with clause\nmult(s(X858), X859, 0, X860) :- mult(X858, X859, X859, X860).\nand substitutionX858 -> T555,\nT531 -> s(T555),\nT533 -> 0,\nX859 -> s(s(s(s(s(s(s(0))))))),\nT556 -> 0,\nT535 -> T558,\nX860 -> T558,\nT557 -> T558", fontsize=14, style = filled, fillcolor = lightblue];
286 -> 646 [arrowhead = none ];
646 -> 288;

647 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
286 -> 647 [arrowhead = none ];
647 -> 289;

648 [label="EVAL with clause\nmult(X1023, X1024, s(X1025), s(X1026)) :- mult(X1023, X1024, X1025, X1026).\nand substitutionT531 -> T635,\nX1023 -> T635,\nT533 -> s(T637),\nX1024 -> s(s(s(s(s(s(s(s(T637)))))))),\nX1025 -> T637,\nT636 -> s(T637),\nX1026 -> T639,\nT535 -> s(T639),\nT638 -> T639", fontsize=14, style = filled, fillcolor = lightblue];
287 -> 648 [arrowhead = none ];
648 -> 336;

649 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
287 -> 649 [arrowhead = none ];
649 -> 337;

650 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
288 -> 650 [arrowhead = none ];
650 -> 290;

651 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
290 -> 651 [arrowhead = none ];
651 -> 291;

652 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
291 -> 652 [arrowhead = none ];
652 -> 292;

653 [label="EVAL with clause\nmult(X875, X876, s(X877), s(X878)) :- mult(X875, X876, X877, X878).\nand substitutionT555 -> T564,\nX875 -> T564,\nX876 -> s(s(s(s(s(s(s(0))))))),\nX877 -> s(s(s(s(s(s(0)))))),\nX878 -> T566,\nT558 -> s(T566),\nT565 -> T566", fontsize=14, style = filled, fillcolor = lightblue];
292 -> 653 [arrowhead = none ];
653 -> 293;

654 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
292 -> 654 [arrowhead = none ];
654 -> 294;

655 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
293 -> 655 [arrowhead = none ];
655 -> 295;

656 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
295 -> 656 [arrowhead = none ];
656 -> 296;

657 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
296 -> 657 [arrowhead = none ];
657 -> 297;

658 [label="EVAL with clause\nmult(X893, X894, s(X895), s(X896)) :- mult(X893, X894, X895, X896).\nand substitutionT564 -> T572,\nX893 -> T572,\nX894 -> s(s(s(s(s(s(s(0))))))),\nX895 -> s(s(s(s(s(0))))),\nX896 -> T574,\nT566 -> s(T574),\nT573 -> T574", fontsize=14, style = filled, fillcolor = lightblue];
297 -> 658 [arrowhead = none ];
658 -> 298;

659 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
297 -> 659 [arrowhead = none ];
659 -> 299;

660 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
298 -> 660 [arrowhead = none ];
660 -> 300;

661 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
300 -> 661 [arrowhead = none ];
661 -> 301;

662 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
301 -> 662 [arrowhead = none ];
662 -> 302;

663 [label="EVAL with clause\nmult(X911, X912, s(X913), s(X914)) :- mult(X911, X912, X913, X914).\nand substitutionT572 -> T580,\nX911 -> T580,\nX912 -> s(s(s(s(s(s(s(0))))))),\nX913 -> s(s(s(s(0)))),\nX914 -> T582,\nT574 -> s(T582),\nT581 -> T582", fontsize=14, style = filled, fillcolor = lightblue];
302 -> 663 [arrowhead = none ];
663 -> 303;

664 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
302 -> 664 [arrowhead = none ];
664 -> 304;

665 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
303 -> 665 [arrowhead = none ];
665 -> 305;

666 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
305 -> 666 [arrowhead = none ];
666 -> 306;

667 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
306 -> 667 [arrowhead = none ];
667 -> 307;

668 [label="EVAL with clause\nmult(X929, X930, s(X931), s(X932)) :- mult(X929, X930, X931, X932).\nand substitutionT580 -> T588,\nX929 -> T588,\nX930 -> s(s(s(s(s(s(s(0))))))),\nX931 -> s(s(s(0))),\nX932 -> T590,\nT582 -> s(T590),\nT589 -> T590", fontsize=14, style = filled, fillcolor = lightblue];
307 -> 668 [arrowhead = none ];
668 -> 308;

669 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
307 -> 669 [arrowhead = none ];
669 -> 309;

670 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
308 -> 670 [arrowhead = none ];
670 -> 310;

671 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
310 -> 671 [arrowhead = none ];
671 -> 311;

672 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
311 -> 672 [arrowhead = none ];
672 -> 312;

673 [label="EVAL with clause\nmult(X947, X948, s(X949), s(X950)) :- mult(X947, X948, X949, X950).\nand substitutionT588 -> T596,\nX947 -> T596,\nX948 -> s(s(s(s(s(s(s(0))))))),\nX949 -> s(s(0)),\nX950 -> T598,\nT590 -> s(T598),\nT597 -> T598", fontsize=14, style = filled, fillcolor = lightblue];
312 -> 673 [arrowhead = none ];
673 -> 313;

674 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
312 -> 674 [arrowhead = none ];
674 -> 314;

675 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
313 -> 675 [arrowhead = none ];
675 -> 315;

676 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
315 -> 676 [arrowhead = none ];
676 -> 316;

677 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
316 -> 677 [arrowhead = none ];
677 -> 317;

678 [label="EVAL with clause\nmult(X965, X966, s(X967), s(X968)) :- mult(X965, X966, X967, X968).\nand substitutionT596 -> T604,\nX965 -> T604,\nX966 -> s(s(s(s(s(s(s(0))))))),\nX967 -> s(0),\nX968 -> T606,\nT598 -> s(T606),\nT605 -> T606", fontsize=14, style = filled, fillcolor = lightblue];
317 -> 678 [arrowhead = none ];
678 -> 318;

679 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
317 -> 679 [arrowhead = none ];
679 -> 319;

680 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
318 -> 680 [arrowhead = none ];
680 -> 320;

681 [label="BACKTRACK\nfor clause: mult(0, Y, 0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
320 -> 681 [arrowhead = none ];
681 -> 321;

682 [label="BACKTRACK\nfor clause: mult(s(U), Y, 0, Z) :- mult(U, Y, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
321 -> 682 [arrowhead = none ];
682 -> 322;

683 [label="EVAL with clause\nmult(X983, X984, s(X985), s(X986)) :- mult(X983, X984, X985, X986).\nand substitutionT604 -> T612,\nX983 -> T612,\nX984 -> s(s(s(s(s(s(s(0))))))),\nX985 -> 0,\nX986 -> T614,\nT606 -> s(T614),\nT613 -> T614", fontsize=14, style = filled, fillcolor = lightblue];
322 -> 683 [arrowhead = none ];
683 -> 323;

684 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
322 -> 684 [arrowhead = none ];
684 -> 324;

685 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
323 -> 685 [arrowhead = none ];
685 -> 325;

686 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
325 -> 686 [arrowhead = none ];
686 -> 326;

687 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
325 -> 687 [arrowhead = none ];
687 -> 327;

688 [label="EVAL with clause\nmult(0, X993, 0, 0).\nand substitutionT612 -> 0,\nX993 -> s(s(s(s(s(s(s(0))))))),\nT614 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
326 -> 688 [arrowhead = none ];
688 -> 328;

689 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
326 -> 689 [arrowhead = none ];
689 -> 329;

690 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
327 -> 690 [arrowhead = none ];
690 -> 331;

691 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
327 -> 691 [arrowhead = none ];
691 -> 332;

692 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
328 -> 692 [arrowhead = none ];
692 -> 330;

693 [label="EVAL with clause\nmult(s(X1006), X1007, 0, X1008) :- mult(X1006, X1007, X1007, X1008).\nand substitutionX1006 -> T623,\nT612 -> s(T623),\nX1007 -> s(s(s(s(s(s(s(0))))))),\nT614 -> T625,\nX1008 -> T625,\nT624 -> T625", fontsize=14, style = filled, fillcolor = lightblue];
331 -> 693 [arrowhead = none ];
693 -> 333;

694 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
331 -> 694 [arrowhead = none ];
694 -> 334;

695 [label="BACKTRACK\nfor clause: mult(X, Y, s(W), s(Z)) :- mult(X, Y, W, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
332 -> 695 [arrowhead = none ];
695 -> 335;

696 [label="INSTANCE with matching:\nT555 -> T623\nT558 -> T625", fontsize=14, style = filled, fillcolor = lightgrey];
333 -> 696 [arrowhead = none , style=dashed];
696 -> 288[style=dashed];

697 [label="GENERALIZATION\nT642 <-- s(s(s(s(s(s(s(T637)))))))\n\nNew Knowledge:\nT642 is ground", fontsize=14, style = filled, fillcolor = violet];
336 -> 697 [arrowhead = none ];
697 -> 338;

698 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
338 -> 698 [arrowhead = none ];
698 -> 339;

699 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
339 -> 699 [arrowhead = none ];
699 -> 340;

700 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
339 -> 700 [arrowhead = none ];
700 -> 341;

701 [label="EVAL with clause\nmult(0, X1035, 0, 0).\nand substitutionT635 -> 0,\nT642 -> T649,\nX1035 -> s(T649),\nT637 -> 0,\nT639 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
340 -> 701 [arrowhead = none ];
701 -> 342;

702 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
340 -> 702 [arrowhead = none ];
702 -> 343;

703 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
341 -> 703 [arrowhead = none ];
703 -> 345;

704 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
341 -> 704 [arrowhead = none ];
704 -> 346;

705 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
342 -> 705 [arrowhead = none ];
705 -> 344;

706 [label="EVAL with clause\nmult(s(X1048), X1049, 0, X1050) :- mult(X1048, X1049, X1049, X1050).\nand substitutionX1048 -> T662,\nT635 -> s(T662),\nT642 -> T663,\nX1049 -> s(T663),\nT637 -> 0,\nT639 -> T665,\nX1050 -> T665,\nT664 -> T665", fontsize=14, style = filled, fillcolor = lightblue];
345 -> 706 [arrowhead = none ];
706 -> 347;

707 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
345 -> 707 [arrowhead = none ];
707 -> 348;

708 [label="EVAL with clause\nmult(X1061, X1062, s(X1063), s(X1064)) :- mult(X1061, X1062, X1063, X1064).\nand substitutionT635 -> T676,\nX1061 -> T676,\nT642 -> T677,\nX1062 -> s(T677),\nX1063 -> T678,\nT637 -> s(T678),\nX1064 -> T680,\nT639 -> s(T680),\nT679 -> T680", fontsize=14, style = filled, fillcolor = lightblue];
346 -> 708 [arrowhead = none ];
708 -> 349;

709 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
346 -> 709 [arrowhead = none ];
709 -> 350;

710 [label="INSTANCE with matching:\nT28 -> T662\nT29 -> s(T663)\nT31 -> T665", fontsize=14, style = filled, fillcolor = lightgrey];
347 -> 710 [arrowhead = none , style=dashed];
710 -> 12[style=dashed];

711 [label="INSTANCE with matching:\nT635 -> T676\nT642 -> T677\nT637 -> T678\nT639 -> T680", fontsize=14, style = filled, fillcolor = lightgrey];
349 -> 711 [arrowhead = none , style=dashed];
711 -> 338[style=dashed];

}

(2) Obligation:

Triples:

multA(s(X1), X2) :- multA(X1, X2).
multB(s(X1), s(X2)) :- multB(X1, X2).
multC(s(X1), s(s(X2))) :- multC(X1, X2).
multD(s(X1), s(s(s(X2)))) :- multD(X1, X2).
multE(s(X1), s(s(s(s(X2))))) :- multE(X1, X2).
multF(s(X1), s(s(s(s(s(X2)))))) :- multF(X1, X2).
multG(s(X1), s(s(s(s(s(s(X2))))))) :- multG(X1, X2).
multH(s(X1), s(s(s(s(s(s(s(X2)))))))) :- multH(X1, X2).
multI(s(X1), 0, X2) :- multA(X1, X2).
multI(s(X1), s(0), s(X2)) :- multB(X1, X2).
multI(s(X1), s(s(0)), s(s(X2))) :- multC(X1, X2).
multI(s(X1), s(s(s(0))), s(s(s(X2)))) :- multD(X1, X2).
multI(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) :- multE(X1, X2).
multI(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) :- multF(X1, X2).
multI(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) :- multG(X1, X2).
multI(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) :- multH(X1, X2).
multI(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) :- multJ(X1, s(s(s(s(s(s(s(X2))))))), X2, X3).
multJ(s(X1), X2, 0, X3) :- multI(X1, s(X2), X3).
multJ(X1, X2, s(X3), s(X4)) :- multJ(X1, X2, X3, X4).
timesK(s(X1), X2, X3) :- multI(X1, X2, X3).

Clauses:

multcA(0, 0).
multcA(s(X1), X2) :- multcA(X1, X2).
multcB(0, s(0)).
multcB(s(X1), s(X2)) :- multcB(X1, X2).
multcC(0, s(s(0))).
multcC(s(X1), s(s(X2))) :- multcC(X1, X2).
multcD(0, s(s(s(0)))).
multcD(s(X1), s(s(s(X2)))) :- multcD(X1, X2).
multcE(0, s(s(s(s(0))))).
multcE(s(X1), s(s(s(s(X2))))) :- multcE(X1, X2).
multcF(0, s(s(s(s(s(0)))))).
multcF(s(X1), s(s(s(s(s(X2)))))) :- multcF(X1, X2).
multcG(0, s(s(s(s(s(s(0))))))).
multcG(s(X1), s(s(s(s(s(s(X2))))))) :- multcG(X1, X2).
multcH(0, s(s(s(s(s(s(s(0)))))))).
multcH(s(X1), s(s(s(s(s(s(s(X2)))))))) :- multcH(X1, X2).
multcI(0, 0, 0).
multcI(s(X1), 0, X2) :- multcA(X1, X2).
multcI(0, s(0), s(0)).
multcI(s(X1), s(0), s(X2)) :- multcB(X1, X2).
multcI(0, s(s(0)), s(s(0))).
multcI(s(X1), s(s(0)), s(s(X2))) :- multcC(X1, X2).
multcI(0, s(s(s(0))), s(s(s(0)))).
multcI(s(X1), s(s(s(0))), s(s(s(X2)))) :- multcD(X1, X2).
multcI(0, s(s(s(s(0)))), s(s(s(s(0))))).
multcI(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) :- multcE(X1, X2).
multcI(0, s(s(s(s(s(0))))), s(s(s(s(s(0)))))).
multcI(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) :- multcF(X1, X2).
multcI(0, s(s(s(s(s(s(0)))))), s(s(s(s(s(s(0))))))).
multcI(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) :- multcG(X1, X2).
multcI(0, s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(0)))))))).
multcI(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) :- multcH(X1, X2).
multcI(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) :- multcJ(X1, s(s(s(s(s(s(s(X2))))))), X2, X3).
multcJ(0, X1, 0, 0).
multcJ(s(X1), X2, 0, X3) :- multcI(X1, s(X2), X3).
multcJ(X1, X2, s(X3), s(X4)) :- multcJ(X1, X2, X3, X4).

Afs:

timesK(x1, x2, x3)  =  timesK(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
timesK_in: (b,b,f)
multI_in: (b,b,f)
multA_in: (b,f)
multB_in: (b,f)
multC_in: (b,f)
multD_in: (b,f)
multE_in: (b,f)
multF_in: (b,f)
multG_in: (b,f)
multH_in: (b,f)
multJ_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

TIMESK_IN_GGA(s(X1), X2, X3) → U20_GGA(X1, X2, X3, multI_in_gga(X1, X2, X3))
TIMESK_IN_GGA(s(X1), X2, X3) → MULTI_IN_GGA(X1, X2, X3)
MULTI_IN_GGA(s(X1), 0, X2) → U9_GGA(X1, X2, multA_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), 0, X2) → MULTA_IN_GA(X1, X2)
MULTA_IN_GA(s(X1), X2) → U1_GA(X1, X2, multA_in_ga(X1, X2))
MULTA_IN_GA(s(X1), X2) → MULTA_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(0), s(X2)) → U10_GGA(X1, X2, multB_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(0), s(X2)) → MULTB_IN_GA(X1, X2)
MULTB_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, multB_in_ga(X1, X2))
MULTB_IN_GA(s(X1), s(X2)) → MULTB_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(0)), s(s(X2))) → U11_GGA(X1, X2, multC_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(0)), s(s(X2))) → MULTC_IN_GA(X1, X2)
MULTC_IN_GA(s(X1), s(s(X2))) → U3_GA(X1, X2, multC_in_ga(X1, X2))
MULTC_IN_GA(s(X1), s(s(X2))) → MULTC_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(0))), s(s(s(X2)))) → U12_GGA(X1, X2, multD_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(0))), s(s(s(X2)))) → MULTD_IN_GA(X1, X2)
MULTD_IN_GA(s(X1), s(s(s(X2)))) → U4_GA(X1, X2, multD_in_ga(X1, X2))
MULTD_IN_GA(s(X1), s(s(s(X2)))) → MULTD_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) → U13_GGA(X1, X2, multE_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) → MULTE_IN_GA(X1, X2)
MULTE_IN_GA(s(X1), s(s(s(s(X2))))) → U5_GA(X1, X2, multE_in_ga(X1, X2))
MULTE_IN_GA(s(X1), s(s(s(s(X2))))) → MULTE_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) → U14_GGA(X1, X2, multF_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) → MULTF_IN_GA(X1, X2)
MULTF_IN_GA(s(X1), s(s(s(s(s(X2)))))) → U6_GA(X1, X2, multF_in_ga(X1, X2))
MULTF_IN_GA(s(X1), s(s(s(s(s(X2)))))) → MULTF_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) → U15_GGA(X1, X2, multG_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) → MULTG_IN_GA(X1, X2)
MULTG_IN_GA(s(X1), s(s(s(s(s(s(X2))))))) → U7_GA(X1, X2, multG_in_ga(X1, X2))
MULTG_IN_GA(s(X1), s(s(s(s(s(s(X2))))))) → MULTG_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) → U16_GGA(X1, X2, multH_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) → MULTH_IN_GA(X1, X2)
MULTH_IN_GA(s(X1), s(s(s(s(s(s(s(X2)))))))) → U8_GA(X1, X2, multH_in_ga(X1, X2))
MULTH_IN_GA(s(X1), s(s(s(s(s(s(s(X2)))))))) → MULTH_IN_GA(X1, X2)
MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) → U17_GGA(X1, X2, X3, multJ_in_ggga(X1, s(s(s(s(s(s(s(X2))))))), X2, X3))
MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) → MULTJ_IN_GGGA(X1, s(s(s(s(s(s(s(X2))))))), X2, X3)
MULTJ_IN_GGGA(s(X1), X2, 0, X3) → U18_GGGA(X1, X2, X3, multI_in_gga(X1, s(X2), X3))
MULTJ_IN_GGGA(s(X1), X2, 0, X3) → MULTI_IN_GGA(X1, s(X2), X3)
MULTJ_IN_GGGA(X1, X2, s(X3), s(X4)) → U19_GGGA(X1, X2, X3, X4, multJ_in_ggga(X1, X2, X3, X4))
MULTJ_IN_GGGA(X1, X2, s(X3), s(X4)) → MULTJ_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
0  =  0
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x1, x2, x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

TIMESK_IN_GGA(s(X1), X2, X3) → U20_GGA(X1, X2, X3, multI_in_gga(X1, X2, X3))
TIMESK_IN_GGA(s(X1), X2, X3) → MULTI_IN_GGA(X1, X2, X3)
MULTI_IN_GGA(s(X1), 0, X2) → U9_GGA(X1, X2, multA_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), 0, X2) → MULTA_IN_GA(X1, X2)
MULTA_IN_GA(s(X1), X2) → U1_GA(X1, X2, multA_in_ga(X1, X2))
MULTA_IN_GA(s(X1), X2) → MULTA_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(0), s(X2)) → U10_GGA(X1, X2, multB_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(0), s(X2)) → MULTB_IN_GA(X1, X2)
MULTB_IN_GA(s(X1), s(X2)) → U2_GA(X1, X2, multB_in_ga(X1, X2))
MULTB_IN_GA(s(X1), s(X2)) → MULTB_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(0)), s(s(X2))) → U11_GGA(X1, X2, multC_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(0)), s(s(X2))) → MULTC_IN_GA(X1, X2)
MULTC_IN_GA(s(X1), s(s(X2))) → U3_GA(X1, X2, multC_in_ga(X1, X2))
MULTC_IN_GA(s(X1), s(s(X2))) → MULTC_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(0))), s(s(s(X2)))) → U12_GGA(X1, X2, multD_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(0))), s(s(s(X2)))) → MULTD_IN_GA(X1, X2)
MULTD_IN_GA(s(X1), s(s(s(X2)))) → U4_GA(X1, X2, multD_in_ga(X1, X2))
MULTD_IN_GA(s(X1), s(s(s(X2)))) → MULTD_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) → U13_GGA(X1, X2, multE_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(0)))), s(s(s(s(X2))))) → MULTE_IN_GA(X1, X2)
MULTE_IN_GA(s(X1), s(s(s(s(X2))))) → U5_GA(X1, X2, multE_in_ga(X1, X2))
MULTE_IN_GA(s(X1), s(s(s(s(X2))))) → MULTE_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) → U14_GGA(X1, X2, multF_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(0))))), s(s(s(s(s(X2)))))) → MULTF_IN_GA(X1, X2)
MULTF_IN_GA(s(X1), s(s(s(s(s(X2)))))) → U6_GA(X1, X2, multF_in_ga(X1, X2))
MULTF_IN_GA(s(X1), s(s(s(s(s(X2)))))) → MULTF_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) → U15_GGA(X1, X2, multG_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(0)))))), s(s(s(s(s(s(X2))))))) → MULTG_IN_GA(X1, X2)
MULTG_IN_GA(s(X1), s(s(s(s(s(s(X2))))))) → U7_GA(X1, X2, multG_in_ga(X1, X2))
MULTG_IN_GA(s(X1), s(s(s(s(s(s(X2))))))) → MULTG_IN_GA(X1, X2)
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) → U16_GGA(X1, X2, multH_in_ga(X1, X2))
MULTI_IN_GGA(s(X1), s(s(s(s(s(s(s(0))))))), s(s(s(s(s(s(s(X2)))))))) → MULTH_IN_GA(X1, X2)
MULTH_IN_GA(s(X1), s(s(s(s(s(s(s(X2)))))))) → U8_GA(X1, X2, multH_in_ga(X1, X2))
MULTH_IN_GA(s(X1), s(s(s(s(s(s(s(X2)))))))) → MULTH_IN_GA(X1, X2)
MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) → U17_GGA(X1, X2, X3, multJ_in_ggga(X1, s(s(s(s(s(s(s(X2))))))), X2, X3))
MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) → MULTJ_IN_GGGA(X1, s(s(s(s(s(s(s(X2))))))), X2, X3)
MULTJ_IN_GGGA(s(X1), X2, 0, X3) → U18_GGGA(X1, X2, X3, multI_in_gga(X1, s(X2), X3))
MULTJ_IN_GGGA(s(X1), X2, 0, X3) → MULTI_IN_GGA(X1, s(X2), X3)
MULTJ_IN_GGGA(X1, X2, s(X3), s(X4)) → U19_GGGA(X1, X2, X3, X4, multJ_in_ggga(X1, X2, X3, X4))
MULTJ_IN_GGGA(X1, X2, s(X3), s(X4)) → MULTJ_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
multI_in_gga(x1, x2, x3)  =  multI_in_gga(x1, x2)
0  =  0
multA_in_ga(x1, x2)  =  multA_in_ga(x1)
multB_in_ga(x1, x2)  =  multB_in_ga(x1)
multC_in_ga(x1, x2)  =  multC_in_ga(x1)
multD_in_ga(x1, x2)  =  multD_in_ga(x1)
multE_in_ga(x1, x2)  =  multE_in_ga(x1)
multF_in_ga(x1, x2)  =  multF_in_ga(x1)
multG_in_ga(x1, x2)  =  multG_in_ga(x1)
multH_in_ga(x1, x2)  =  multH_in_ga(x1)
multJ_in_ggga(x1, x2, x3, x4)  =  multJ_in_ggga(x1, x2, x3)
TIMESK_IN_GGA(x1, x2, x3)  =  TIMESK_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x1, x3)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x1, x3)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)
U18_GGGA(x1, x2, x3, x4)  =  U18_GGGA(x1, x2, x4)
U19_GGGA(x1, x2, x3, x4, x5)  =  U19_GGGA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 9 SCCs with 29 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(X1), s(s(s(s(s(s(s(X2)))))))) → MULTH_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTH_IN_GA(x1, x2)  =  MULTH_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTH_IN_GA(s(X1)) → MULTH_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTH_IN_GA(s(X1)) → MULTH_IN_GA(X1)
  The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(X1), s(s(s(s(s(s(X2))))))) → MULTG_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTG_IN_GA(x1, x2)  =  MULTG_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTG_IN_GA(s(X1)) → MULTG_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTG_IN_GA(s(X1)) → MULTG_IN_GA(X1)
  The graph contains the following edges 1 > 1

(16) YES

(17) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(X1), s(s(s(s(s(X2)))))) → MULTF_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTF_IN_GA(x1, x2)  =  MULTF_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(18) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(19) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTF_IN_GA(s(X1)) → MULTF_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(20) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTF_IN_GA(s(X1)) → MULTF_IN_GA(X1)
  The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(X1), s(s(s(s(X2))))) → MULTE_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTE_IN_GA(x1, x2)  =  MULTE_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(23) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(24) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTE_IN_GA(s(X1)) → MULTE_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(25) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTE_IN_GA(s(X1)) → MULTE_IN_GA(X1)
  The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(X1), s(s(s(X2)))) → MULTD_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTD_IN_GA(x1, x2)  =  MULTD_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(28) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(29) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTD_IN_GA(s(X1)) → MULTD_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(30) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTD_IN_GA(s(X1)) → MULTD_IN_GA(X1)
  The graph contains the following edges 1 > 1

(31) YES

(32) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(X1), s(s(X2))) → MULTC_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTC_IN_GA(x1, x2)  =  MULTC_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(33) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(34) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTC_IN_GA(s(X1)) → MULTC_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTC_IN_GA(s(X1)) → MULTC_IN_GA(X1)
  The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTB_IN_GA(s(X1), s(X2)) → MULTB_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTB_IN_GA(x1, x2)  =  MULTB_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(38) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(39) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTB_IN_GA(s(X1)) → MULTB_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(40) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTB_IN_GA(s(X1)) → MULTB_IN_GA(X1)
  The graph contains the following edges 1 > 1

(41) YES

(42) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2)))))))), s(s(s(s(s(s(s(s(X3))))))))) → MULTJ_IN_GGGA(X1, s(s(s(s(s(s(s(X2))))))), X2, X3)
MULTJ_IN_GGGA(s(X1), X2, 0, X3) → MULTI_IN_GGA(X1, s(X2), X3)
MULTJ_IN_GGGA(X1, X2, s(X3), s(X4)) → MULTJ_IN_GGGA(X1, X2, X3, X4)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
MULTI_IN_GGA(x1, x2, x3)  =  MULTI_IN_GGA(x1, x2)
MULTJ_IN_GGGA(x1, x2, x3, x4)  =  MULTJ_IN_GGGA(x1, x2, x3)

We have to consider all (P,R,Pi)-chains

(43) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(44) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2))))))))) → MULTJ_IN_GGGA(X1, s(s(s(s(s(s(s(X2))))))), X2)
MULTJ_IN_GGGA(s(X1), X2, 0) → MULTI_IN_GGA(X1, s(X2))
MULTJ_IN_GGGA(X1, X2, s(X3)) → MULTJ_IN_GGGA(X1, X2, X3)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(45) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTJ_IN_GGGA(s(X1), X2, 0) → MULTI_IN_GGA(X1, s(X2))
  The graph contains the following edges 1 > 1

• MULTJ_IN_GGGA(X1, X2, s(X3)) → MULTJ_IN_GGGA(X1, X2, X3)
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

• MULTI_IN_GGA(X1, s(s(s(s(s(s(s(s(X2))))))))) → MULTJ_IN_GGGA(X1, s(s(s(s(s(s(s(X2))))))), X2)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(46) YES

(47) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

MULTA_IN_GA(s(X1), X2) → MULTA_IN_GA(X1, X2)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
MULTA_IN_GA(x1, x2)  =  MULTA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(48) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(49) Obligation:

Q DP problem:
The TRS P consists of the following rules:

MULTA_IN_GA(s(X1)) → MULTA_IN_GA(X1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(50) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• MULTA_IN_GA(s(X1)) → MULTA_IN_GA(X1)
  The graph contains the following edges 1 > 1

(51) YES